(set-logic QF_BV)
(set-option :model_validate true)
(set-option :model true)
(set-option :smt.mbqi false)
(set-option :smt.arith.eager_eq_axioms true)
(set-option :smt.arith.bprop_on_pivoted_rows true)
(set-option :smt.arith.min true)
(set-option :smt.dack.eq true)
(set-option :smt.arith.random_initial_value false)
(set-option :smt.arith.auto_config_simplex true)
(set-option :smt.theory_aware_branching true)
(set-option :smt.arith.greatest_error_pivot true)
(set-option :smt.arith.int_eq_branch true)
(set-option :sat.asymm_branch.all true)
(set-option :sat.cut.aig true)
(set-option :sat.cce true)
(set-option :sat.abce false)
(set-option :sat.bce true)
(set-option :sat.force_cleanup true)
(set-option :sat.anf false)
(set-option :sat.cut true)
(set-option :sat.cut.npn3 true)
(set-option :sat.bca true)
(set-option :sat.acce true)
(set-option :sat.elim_vars false)
(set-option :sat.scc false)
(set-option :sat.scc.tr true)
(set-option :sat.threads 3)
(set-option :sat.branching.heuristic chb)
(set-option :rewriter.blast_distinct true)
(set-option :model.inline_def true)
(set-option :model.partial false)
(set-option :nlsat.minimize_conflicts false)
(set-option :smt.arith.solver 6)
(set-option :smt.threads 3)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const bv_12-0 (_ BitVec 12))
(declare-const bv_30-0 (_ BitVec 30))
(declare-const v5 Bool)
(push 1)
(declare-const v6 Bool)
(declare-const bv_11-0 (_ BitVec 11))
(pop 1)
(declare-const v7 Bool)
(assert (or v1 v1 v7))
(assert (or v2 v1 v0))
(assert (or v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (=> v0 v1)))
(assert (or v4 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (=> v0 v1)))
(assert (or v3 v4 v0))
(assert (or v0 (=> v0 v1) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v0 v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v3 v2 v3))
(assert (or v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvule bv_30-0 bv_30-0)))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v2 v4))
(assert (or (bvule bv_30-0 bv_30-0) v4 v3))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v2 v2))
(assert (or v3 v7 (=> v0 v1)))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v4))
(assert (or v0 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v7))
(assert (or (bvule bv_30-0 bv_30-0) v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v3 v7 v4))
(assert (or v1 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (bvule bv_30-0 bv_30-0) v0 v0))
(assert (or (bvule bv_30-0 bv_30-0) v1 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (bvule bv_30-0 bv_30-0) v4 v2))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (=> v0 v1) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 v7))
(assert (or (=> v0 v1) v5 v7))
(assert (or (bvule bv_30-0 bv_30-0) (bvule bv_30-0 bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v0 (bvule bv_30-0 bv_30-0) v7))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvule bv_30-0 bv_30-0) v3))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3))
(assert (or v4 (=> v0 v1) (=> v0 v1)))
(assert (or v2 v0 v2))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (=> v0 v1) v1))
(assert (or v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (bvule bv_30-0 bv_30-0) (=> v0 v1) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v0 (=> v0 v1) (bvule bv_30-0 bv_30-0)))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v0 v4))
(assert (or v4 v7 v2))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvule bv_30-0 bv_30-0)))
(assert (or (=> v0 v1) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7))
(assert (or (bvule bv_30-0 bv_30-0) v7 v0))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v5 v4))
(assert (or (bvule bv_30-0 bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3))
(assert (or v3 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v2 v7 v3))
(assert (or v3 (=> v0 v1) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v2 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v4))
(assert (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7))
(assert (or v5 v3 (=> v0 v1)))
(assert (or v5 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v3))
(assert (or v2 v3 (bvule bv_30-0 bv_30-0)))
(assert (or v3 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v3))
(assert (or v4 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (=> v0 v1) v4))
(assert (or (bvule bv_30-0 bv_30-0) v5 v4))
(assert (or (bvule bv_30-0 bv_30-0) v0 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v4 v3))
(assert (or v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v0))
(assert (or (=> v0 v1) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v0))
(assert (or (bvule bv_30-0 bv_30-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v2))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v2 (=> v0 v1)))
(assert (or v2 v4 v7))
(assert (or (=> v0 v1) (bvule bv_30-0 bv_30-0) v2))
(assert (or (=> v0 v1) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v5))
(assert (or v4 v1 v7))
(assert (or v3 v7 v7))
(assert (or v2 v0 v7))
(assert (or v3 v4 v1))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7 v2))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v2 v4 v5))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1 v5))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7 (bvule bv_30-0 bv_30-0)))
(assert (or v0 v4 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v1 (bvule bv_30-0 bv_30-0) v1))
(assert (or v4 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v4 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1))
(assert (or v0 v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v4 (=> v0 v1) (bvule bv_30-0 bv_30-0)))
(assert (or v5 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4))
(assert (or v2 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (=> v0 v1)))
(assert (or v7 v5 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v2 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v7))
(assert (or v0 v0 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v0 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1))
(assert (or v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (=> v0 v1)))
(assert (or (bvule bv_30-0 bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v3))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3 v5))
(assert (or (bvule bv_30-0 bv_30-0) v2 (=> v0 v1)))
(assert (or v5 v7 (bvule bv_30-0 bv_30-0)))
(assert (or v2 v2 v3))
(assert (or v5 v3 v7))
(assert (or v4 (bvule bv_30-0 bv_30-0) v1))
(assert (or v0 v4 v3))
(assert (or (=> v0 v1) v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (=> v0 v1) v7))
(assert (or v4 v2 v7))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or (=> v0 v1) v5 v7))
(assert (or v4 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v2))
(assert (or v4 v1 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v7 v7 (bvule bv_30-0 bv_30-0)))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v0 v0))
(assert (or v1 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (=> v0 v1) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3))
(assert (or v4 v2 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v1 v3))
(assert (or v1 v0 v1))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v1 (bvule bv_30-0 bv_30-0)))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v2 (bvule bv_30-0 bv_30-0)))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7))
(assert (or v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v4 v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3 v3))
(assert (or v3 v0 v7))
(assert (or (=> v0 v1) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0))
(assert (or v3 v2 (=> v0 v1)))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvule bv_30-0 bv_30-0) (=> v0 v1)))
(assert (or v2 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v5))
(assert (or (=> v0 v1) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v2))
(assert (or v1 v3 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v4 v1 v3))
(assert (or v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v5))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (=> v0 v1)))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1))
(assert (or v5 v4 v4))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v2))
(assert (or v3 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v5))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v2 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (bvule bv_30-0 bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (=> v0 v1)))
(assert (or (bvule bv_30-0 bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (=> v0 v1)))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvule bv_30-0 bv_30-0)))
(assert (or v2 v3 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v4 v1 v3))
(assert (or v0 (bvule bv_30-0 bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v4 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v7 v3 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v3 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (=> v0 v1) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (bvule bv_30-0 bv_30-0) v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v4 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v1))
(assert (or v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v4 (bvule bv_30-0 bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v4 (bvule bv_30-0 bv_30-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v5 (=> v0 v1)))
(assert (or v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v2))
(assert (or (bvule bv_30-0 bv_30-0) v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (=> v0 v1) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3))
(assert (or v5 (=> v0 v1) v0))
(assert (or v5 v0 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v1 v5 v0))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v1 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (=> v0 v1) v5 v5))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4))
(assert (or v3 v2 v4))
(assert (or v5 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v1))
(assert (or v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v7 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v2))
(assert (or (bvule bv_30-0 bv_30-0) v1 v3))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v7 v0))
(assert (or v1 (=> v0 v1) v7))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v5 v4))
(assert (or v5 v7 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v1 v7 (bvule bv_30-0 bv_30-0)))
(assert (or v0 v4 (=> v0 v1)))
(assert (or (=> v0 v1) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (=> v0 v1)))
(assert (or v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v3))
(assert (or v7 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v1))
(assert (or v1 v4 (=> v0 v1)))
(assert (or v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4))
(assert (or (=> v0 v1) v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or (=> v0 v1) v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v0 v3))
(assert (or v4 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v4))
(assert (or v7 v3 v5))
(assert (or v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v0))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1 v1))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v0))
(assert (or v7 v2 v2))
(assert (or (bvule bv_30-0 bv_30-0) v7 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v4 v1 v1))
(assert (or v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (bvule bv_30-0 bv_30-0) (=> v0 v1) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 v1))
(assert (or v7 v4 v7))
(assert (or v3 v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v2 v0))
(assert (or v2 v3 v2))
(assert (or v4 (bvule bv_30-0 bv_30-0) v3))
(assert (or v1 v2 v5))
(assert (or v3 v5 v3))
(assert (or v3 v4 v4))
(assert (or v1 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v0))
(assert (or v2 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (=> v0 v1) (bvule bv_30-0 bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v4))
(assert (or v3 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v2))
(assert (or v1 v3 v2))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v0 v3 v0))
(assert (or v0 v0 v2))
(assert (or (bvule bv_30-0 bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v1 v2))
(assert (or (bvule bv_30-0 bv_30-0) v7 v4))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v0))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4))
(assert (or (bvule bv_30-0 bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v2))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v5 v1))
(assert (or (bvule bv_30-0 bv_30-0) v4 v0))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7 (bvule bv_30-0 bv_30-0)))
(assert (or v4 (bvule bv_30-0 bv_30-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (=> v0 v1) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v5 v0 v4))
(assert (or v1 v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (bvule bv_30-0 bv_30-0) v5 v0))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 v5))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvule bv_30-0 bv_30-0) v0))
(assert (or (=> v0 v1) (=> v0 v1) v3))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v5 v2 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or (bvule bv_30-0 bv_30-0) (bvule bv_30-0 bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v3 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v5 v3 v2))
(assert (or v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvule bv_30-0 bv_30-0)))
(assert (or v5 v2 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7 v3))
(assert (or (bvule bv_30-0 bv_30-0) v4 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v5 (=> v0 v1) v5))
(assert (or v5 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v5 (=> v0 v1) v3))
(assert (or (=> v0 v1) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v1 (bvule bv_30-0 bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v0 (=> v0 v1) v4))
(assert (or (bvule bv_30-0 bv_30-0) (bvule bv_30-0 bv_30-0) (bvule bv_30-0 bv_30-0)))
(assert (or v5 v7 v2))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7))
(assert (or v2 (=> v0 v1) v2))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v5))
(assert (or v5 v0 v1))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v1 (=> v0 v1)))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v7 v5 v4))
(assert (or v2 v1 v5))
(assert (or (bvule bv_30-0 bv_30-0) v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v1 v0 v2))
(assert (or (=> v0 v1) v5 v5))
(assert (or v3 v5 v7))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (=> v0 v1)))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (bvule bv_30-0 bv_30-0) v1))
(assert (or (=> v0 v1) v7 v0))
(assert (or v7 v7 v2))
(assert (or (bvule bv_30-0 bv_30-0) (=> v0 v1) v3))
(assert (or v5 v2 v3))
(assert (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7))
(assert (or v0 (bvule bv_30-0 bv_30-0) (bvule bv_30-0 bv_30-0)))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v4 v4))
(assert (or v4 v1 (=> v0 v1)))
(assert (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0))
(assert (or v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3))
(assert (or v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvule bv_30-0 bv_30-0)))
(assert (or v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v5 v1 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v7))
(assert (or (bvule bv_30-0 bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (=> v0 v1)))
(assert (or v7 v5 v2))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3))
(assert (or v3 v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v0 v1 v2))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7 v1))
(assert (or v5 v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (=> v0 v1) v2))
(assert (or (bvule bv_30-0 bv_30-0) v4 v4))
(assert (or v7 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v5))
(assert (or v5 v7 v4))
(assert (or v7 v3 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v4 (bvule bv_30-0 bv_30-0) v4))
(assert (or (=> v0 v1) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (=> v0 v1)))
(assert (or v7 (bvule bv_30-0 bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3 (=> v0 v1)))
(assert (or (bvule bv_30-0 bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (=> v0 v1)))
(assert (or v5 v0 v0))
(assert (or (bvule bv_30-0 bv_30-0) (=> v0 v1) v7))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v5 v5))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v1))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v3 v5))
(assert (or v4 v1 v3))
(assert (or v7 v7 v3))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvule bv_30-0 bv_30-0)))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (=> v0 v1) (bvule bv_30-0 bv_30-0)))
(assert (or (bvule bv_30-0 bv_30-0) v1 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (=> v0 v1) v3 v0))
(assert (or v0 v2 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v0))
(assert (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v5 v4 (bvule bv_30-0 bv_30-0)))
(assert (or v7 v2 v7))
(assert (or v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvule bv_30-0 bv_30-0)))
(assert (or v4 v4 (=> v0 v1)))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v2))
(assert (or v2 v5 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v3 v2 v3))
(assert (or v7 v5 v1))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1))
(assert (or (bvule bv_30-0 bv_30-0) v3 v5))
(assert (or v5 v4 v2))
(assert (or (bvule bv_30-0 bv_30-0) v0 v7))
(assert (or v3 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or (bvule bv_30-0 bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v7))
(assert (or v7 v3 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3 v1))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v0 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v0 v5 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (or v4 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))
(assert (or v7 v1 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v7 v3 v0))
(assert (or v5 v4 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or v4 v7 v0))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (bvule bv_30-0 bv_30-0) v7))
(assert (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0 v4))
(assert (or v1 v5 v3))
(assert (=> (or v1 v4 (=> v0 v1)) (or (=> v0 v1) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)))))
(assert (or (or v2 (=> v0 v1) v2) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)))))
(assert (or (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or v5 v4 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v5 v7 v4)))
(assert (=> (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0 v4) (or (bvule bv_30-0 bv_30-0) v4 v4)))
(assert (or (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3 v3) (or v3 v5 v3)))
(assert (and (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0) (or v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)))))
(assert (or (or v7 v3 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or v5 v7 (bvule bv_30-0 bv_30-0)) (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v2 v4 v7) (or v3 v4 v4) (or v3 v7 v7) (or (bvule bv_30-0 bv_30-0) v0 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (=> v0 v1) v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or v1 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7)))
(assert (=> (or v4 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1) (or v5 (=> v0 v1) v3)))
(assert (or (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)))))
(assert (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0))
(assert (=> (or (=> v0 v1) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (=> v0 v1) v1)))
(assert (or (or (bvule bv_30-0 bv_30-0) v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (bvule bv_30-0 bv_30-0) v4 v2)))
(assert (or (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (bvule bv_30-0 bv_30-0) v2 (=> v0 v1)) (or v7 v5 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v1) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v0 v3) (or (bvule bv_30-0 bv_30-0) v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvule bv_30-0 bv_30-0) (=> v0 v1)) (or v1 v2 v5)))
(assert (=> (or v4 v2 v7) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)))))
(assert (or (or v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvule bv_30-0 bv_30-0)) (or v7 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v2)))
(assert (or (=> v0 v1) (bvule bv_30-0 bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))))
(assert (=> (or v1 v4 (=> v0 v1)) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v2)))
(assert (or (or v3 v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or v5 v3 v7)))
(assert (=> (or v5 v4 (bvule bv_30-0 bv_30-0)) (or v3 v7 v7)))
(assert (or (or v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvule bv_30-0 bv_30-0)) (or v5 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v3)))
(assert (and (or (bvule bv_30-0 bv_30-0) (bvule bv_30-0 bv_30-0) (bvule bv_30-0 bv_30-0)) (or v5 v2 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvule bv_30-0 bv_30-0)) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v0 v0) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v2 v4)))
(assert (or (or (bvule bv_30-0 bv_30-0) v2 (=> v0 v1)) (or v2 (=> v0 v1) v2) (or v0 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1) (or v1 v1 v7) (or v1 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or v5 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v3) (or v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v5 v0 v0)))
(assert (or v5 v0 v4))
(assert (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (=> v0 v1) v5 v7))
(assert (=> (or v5 v4 v2) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7 (bvule bv_30-0 bv_30-0))))
(assert (or (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v4) (or (bvule bv_30-0 bv_30-0) v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)))))
(assert (and (or v4 v1 (=> v0 v1)) (or v2 v0 v2)))
(assert (=> (or v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v0) (or v3 v4 v1)))
(assert (or (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3 v3) (or (bvule bv_30-0 bv_30-0) v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)))))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v2 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (=> (or (=> v0 v1) v5 v7) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)))))
(assert (or (or v0 v5 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0))))
(assert (and (or v4 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (=> v0 v1) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3) (or v5 v0 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v2 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v0 v4 v3) (or (or (bvule bv_30-0 bv_30-0) v2 (=> v0 v1)) (or v2 (=> v0 v1) v2) (or v0 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1) (or v1 v1 v7) (or v1 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or v5 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v3) (or v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v5 v0 v0))))
(assert (or v5 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4))
(assert (=> (or v2 v4 v7) (or v0 (bvule bv_30-0 bv_30-0) (bvule bv_30-0 bv_30-0))))
(assert (or (or (bvule bv_30-0 bv_30-0) v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v4 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v1)))
(assert (or (=> v0 v1) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4))
(assert (=> (or v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or v7 v5 v2)))
(assert (or (or v2 v4 v7) (or v1 v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0))))
(assert (and (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v1 (=> v0 v1)) (or v4 v7 v0) (or v1 v1 v7) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7 (bvule bv_30-0 bv_30-0)) (or v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v2) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v5 (=> v0 v1)) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or v3 v5 v3) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v4)))
(assert (or (or v4 (bvule bv_30-0 bv_30-0) v1) (or v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v2) (or (bvule bv_30-0 bv_30-0) (=> v0 v1) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)))))
(assert (and (or v7 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v1) (or v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvule bv_30-0 bv_30-0)) (or v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v5) (or v4 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (=> v0 v1)) (or v0 v1 v2) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v7 v0) (or v3 v7 v4) (or (bvule bv_30-0 bv_30-0) v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v7 v2 v2) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3) (or v3 v2 v4)))
(assert (=> (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7 (bvule bv_30-0 bv_30-0)) (or v0 v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)))))
(assert (or (or v0 v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or v7 v5 v2)))
(assert (and (or v2 v1 v0) (or v1 (bvule bv_30-0 bv_30-0) v1) (or v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v2) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4) (or v3 v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v5)))
(assert (=> (or v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (and (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4) (or (bvule bv_30-0 bv_30-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v2) (or v3 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v0) (or v5 v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3) (or (bvule bv_30-0 bv_30-0) v0 v7) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or v5 v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or v4 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1 v5))))
(assert (or (or v4 v1 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v5 (=> v0 v1))))
(assert (and (or v4 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7 v1) (or v2 v4 v5) (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v0)))
(assert (=> (or v5 (=> v0 v1) v0) (or v7 v3 v0)))
(assert (or (or (bvule bv_30-0 bv_30-0) v4 v0) (or v0 v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)))))
(assert (and (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7) (or v5 v0 v0) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v1 v3) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v4 v3) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (=> v0 v1)) (or (bvule bv_30-0 bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v3) (or v2 v0 v2)))
(assert (=> (or v0 v0 v2) (or v5 v0 v1)))
(assert (or (or v4 v7 v2) (or v2 v0 v2)))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3 (=> v0 v1)))
(assert (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 v1))
(assert (or v5 (=> v0 v1) v5))
(assert (or (or (or (bvule bv_30-0 bv_30-0) v2 (=> v0 v1)) (or v2 (=> v0 v1) v2) (or v0 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1) (or v1 v1 v7) (or v1 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or v5 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v3) (or v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v5 v0 v0)) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 v1) (or v7 v2 v2) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7 v1) (or (or v4 (bvule bv_30-0 bv_30-0) v1) (or v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v2) (or (bvule bv_30-0 bv_30-0) (=> v0 v1) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)))) (and (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7 v3) (=> (or v1 v4 (=> v0 v1)) (or (=> v0 v1) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)))) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v7 v3) (or v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or v1 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v1 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or v0 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or v1 v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 v1) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (=> v0 v1)))))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4))
(assert (and (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or (=> v0 v1) v5 v7) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0 v4) (or v1 v7 (bvule bv_30-0 bv_30-0)) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (=> v0 v1)) (or v5 v0 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v5 v4 (bvule bv_30-0 bv_30-0)) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7 v1) (or (=> v0 v1) v7 v0) (or v5 v3 v7)))
(check-sat)
(assert (or v3 v2 v3))
(assert (and (or v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or v5 v4 v2) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v1 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (bvule bv_30-0 bv_30-0) v7 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (bvule bv_30-0 bv_30-0) v4 v3) (or v4 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v2 v0) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 v7) (or v5 v0 v4)))
(assert (and (or v1 v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v7 v5 v4) (or (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or v3 v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v0) (or v5 (=> v0 v1) v5) (or v5 v4 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)) (or v4 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0))))
(assert (and (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1 v5) (or (=> v0 v1) v5 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or (=> v0 v1) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v2) (or v0 (bvule bv_30-0 bv_30-0) v7) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or v4 (bvule bv_30-0 bv_30-0) v3) (or v1 v0 v1) (or (or v3 v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or v5 v3 v7)) (or v4 (bvule bv_30-0 bv_30-0) v4)))
(assert (or (bvule bv_30-0 bv_30-0) v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))
(assert (or v1 v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (bvule bv_30-0 bv_30-0) v5 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0)))
(assert (or (or (bvule bv_30-0 bv_30-0) v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v5 v1) (or (=> v0 v1) (=> v0 v1) v3) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v2 (bvule bv_30-0 bv_30-0)) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v7) (and (or v1 v1 v7) (or v0 v4 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)))))
(assert (or (or v1 v5 v3) (or (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3 v3) (or (bvule bv_30-0 bv_30-0) v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)))) (or v4 v1 v1) (or (bvule bv_30-0 bv_30-0) v4 v4) (or (bvule bv_30-0 bv_30-0) v5 v0) (or v0 v4 v3) (or v4 v7 v2) (or v5 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4)))
(assert (or (or v7 v7 (bvule bv_30-0 bv_30-0)) (or v0 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or v1 v1 v7) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v0) (or v1 (bvule bv_30-0 bv_30-0) v1) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3 (=> v0 v1)) (=> (or v4 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v1) (or v5 (=> v0 v1) v3)) (or v4 (bvule bv_30-0 bv_30-0) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v7) (or v7 v5 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or v2 v3 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0))))
(assert (=> (or (bvule bv_30-0 bv_30-0) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3 v5)))
(assert (or (or (=> v0 v1) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0))))
(assert (=> (=> (or v1 v4 (=> v0 v1)) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v2)) (or v1 (bvule bv_30-0 bv_30-0) v1)))
(assert (or (or v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvule bv_30-0 bv_30-0)) (or v2 v1 v0)))
(assert (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v5 v1))
(assert (=> (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4 v5) (and (or v7 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) v0) (or v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))))))
(assert (or (or v4 v1 (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (and (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v4) (or v5 v2 v3) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v4 v3) (or v2 v7 v3) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0)) (or (bvule bv_30-0 bv_30-0) v5 v0) (or (bvule bv_30-0 bv_30-0) v2 (=> v0 v1)) (or (=> v0 v1) (=> v0 v1) v3) (or v4 v2 v7) (or v3 (= bv_30-0 bv_30-0 bv_30-0 (bvsub bv_30-0 bv_30-0) bv_30-0) (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0))) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3 v1))))
(assert (and (=> (or v0 v0 v2) (or v5 v0 v1)) (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v3 (=> v0 v1)) (or v5 v3 (=> v0 v1))))
(assert (or v5 v0 v1))
(assert (or v3 v2 v4))
(assert (or (and (or (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v2 (bvule bv_30-0 bv_30-0)) (or v3 (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) v4) (=> (or v5 (=> v0 v1) v0) (or v7 v3 v0)) (or v0 (=> v0 v1) (bvule bv_30-0 bv_30-0)) (or v7 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1))) (or (= bv_12-0 bv_12-0 (bvudiv bv_12-0 bv_12-0)) (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v7)) (or v5 v3 (=> v0 v1)) (or (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) (distinct v3 v2 v1 (bvult (bvudiv bv_12-0 bv_12-0) bv_12-0) v4 v2 (=> v0 v1)) v3)))
(check-sat)
(exit)
